@string{acm = {{ACM} {P}ress}}

@string{acm-address = {{N}ew {Y}ork, {NY}, {USA}}}

@string{aw = {{A}ddison-{W}esley}}

@string{cacm = {{C}ommunications of the {ACM}}}

@string{ecoop = {{P}roceedings of {E}uropean {C}onference on {O}bject-{O}riented {P}rogramming {(ECOOP)}}}

@string{fool = {{P}roceedings of {W}orkshop on {F}oundations of {O}bject-{O}riented {L}anguages {(FOOL)}}}

@string{ftfjp = {{P}roceedings of the {W}orkshop on {F}ormal {T}echniques for {J}ava-like {P}rograms in {E}uropean {C}onference on {O}bject-{O}riented {P}rogramming {(FTfJP)}}}

@string{icse = {{P}roceedings of the {I}nternational {C}onference on {S}oftware {E}ngineering {(ICSE)}}}

@string{iwaco = {{P}roceedings of {I}nternational {W}orkshop on {A}liasing, {C}onfinement, and {O}wnership {(IWACO)}}}

@string{jacm = {{J}ournal of the {ACM} {(JACM)}}}

@string{lncs = {{L}ecture {N}otes in {C}omputer {S}cience {(LNCS)}}}

@string{oopsla = {{P}roceedings of {ACM} {C}onference on {O}bject-{O}riented {P}rogramming, {S}ystems, {L}anguages, and {A}pplications {(OOPSLA)}}}

@string{pldi = {{P}roceedings of the {ACM} {SIGPLAN} {C}onference on {P}rogramming {L}anguage {D}esign and {I}mplementation {(PLDI)}}}

@string{popl = {{P}roceedings of {ACM} {S}ymposium on {P}rinciples of {P}rogramming {L}anguages {(POPL)}}}

@string{sv = {{S}pringer-{V}erlag}}

@string{sv-address = {{B}erlin, {H}eidelberg, {G}ermany}}

@string{toplas = {{ACM} {T}ransactions on {P}rogramming {L}anguages and {S}ystems {(TOPLAS)}}}

@InProceedings{BoyapatiSBR2003,
  author = 	 "Chandrasekhar Boyapati and Alexandru Salcianu and William {Beebee, Jr.} and Martin Rinard",
  title = 	 "Ownership types for safe region-based memory management in real-time Java",
  booktitle = PLDI2003,
  pages = 	 "324--337",
  year = 	 2003,
  address = 	 PLDI2003addr,
  month = 	 PLDI2003date,
}

@InProceedings{PotaninNCB2006,
  author =	 "Alex Potanin and James Noble and Dave Clarke and
                  Robert Biddle",
  title =	 "Generic ownership for generic {Java}",
  booktitle =	 OOPSLA2006,
  pages =	 "311--324",
  year =	 2006,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA2006date,
}

@InProceedings{ClarkD2002,
  author =	 "Dave Clarke and Sophia Drossopoulou",
  title =	 "Ownership, encapsulation and the disjointness of
                  type and effect",
  booktitle =	 OOPSLA2002,
  pages =	 "292--310",
  year =	 2002,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA2002date
}

@Article{DietlM2005,
  author = 	 "Werner Dietl and Peter M{\"u}ller",
  authorASCII =  "Peter Muller / Peter Mueller",
  title = 	 "Universes: Lightweight ownership for {JML}",
  journal = 	 "Journal of Object Technology (JOT)",
  year = 	 2005,
  volume = 	 4,
  number = 	 8,
  pages = 	 "5--32",
  month = 	 oct
}

@InProceedings{BoyapatiLR2002,
  author = 	 "Chandrasekhar Boyapati and Robert Lee and Martin Rinard",
  title = 	 "Ownership types for safe programming:  Preventing data races and deadlocks",
  booktitle = OOPSLA2002,
  pages = 	 "211--230",
  year = 	 2002,
  address = 	 OOPSLA2002addr,
  month = 	 OOPSLA2002date,
}

@InProceedings{PechtchanskiS2002,
  author =	 "Igor Pechtchanski and Vivek Sarkar",
  title =	 "Immutability specification and its applications",
  booktitle =	 JavaGrande2002,
  pages =	 "202--211",
  year =	 2002,
  publisher =	 acm,
  address =	 {Seattle, WA, USA},
  month =	 JavaGrande2002date,
  abstract =	 "A location is said to be immutable if its value and
                  the values of selected locations reachable from it
                  are guaranteed to remain unchanged during a
                  specified time interval. We introduce a framework
                  for immutability specification, and discuss its
                  application to code optimization. Compared to a
                  final declaration, an immutability assertion in our
                  framework can express a richer set of immutability
                  properties along three dimensions --- lifetime,
                  reachability and context. We present a framework for
                  processing and verifying immutability annotations in
                  Java, as well as extending optimizations so as to
                  exploit immutability information. Preliminary
                  experimental results show that a significant number
                  (82\%) of read accesses could potentially be
                  classified as immutable in our framework. Further,
                  use of immutability information yields substantial
                  reductions (33\% to 99\%) in the number of dynamic
                  read accesses, and also measurable speedups in the
                  range of 5\% to 10\% for certain benchmark
                  programs."
}

@Article{Igarashi:2001:FJM,
  author =       "Atsushi Igarashi and Benjamin C. Pierce and Philip
                 Wadler",
  title =        "Featherweight {Java}: a minimal core calculus for
                 {Java} and {GJ}",
  journal =      TOPLAS,
  volume =       "23",
  number =       "3",
  pages =        "396--450",
  month =        may,
  year =         "2001",
  CODEN =        "ATPSDT",
  ISSN =         "0164-0925",
  bibdate =      "Tue Feb 19 15:41:56 MST 2002",
  bibsource =    "http://www.acm.org/pubs/contents/journals/toplas/",
  acknowledgement = ack-nhfb,
}

@InProceedings{BrachaOSW98,
  author =	 "Gilad Bracha and Martin Odersky and David Stoutamire
                  and Philip Wadler",
  title =	 "Making the Future Safe for the Past: Adding
                  Genericity to the {Java} Programming Language",
  booktitle =	 OOPSLA98,
  pages =	 "183--200",
  year =	 1998,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA98date
}

@Article{KnieselT2001,
  author = 	 "G{\"u}nter Kniesel and Dirk Theisen",
  title = 	 "{JAC} --- Access right based encapsulation for {Java}",
  journal = 	 j-spe,
  year = 	 2001,
  volume =	 31,
  number =	 6,
  pages =	 "555--576"
}

@InProceedings{SkoglundW2001,
  author =	 "Mats Skoglund and Tobias Wrigstad",
  title =	 "A mode system for read-only references in {Java}",
  booktitle =	 FTfJP2001,
  NEEDpages =	 "*",
  year =	 2001,
  publisher =	 sv,
  address =	 sv-address,
  month =	 FTfJP2001date,
}

@InProceedings{Boyland2005,
  author =	 "John Boyland",
  title =	 "Why we should not add \texttt{readonly} to {Java}
                  (yet)",
  booktitle =	 FTFJP2005,
  NEEDpages =	 "",
  year =	 2005,
  publisher =	 sv,
  address =	 {Glasgow, Scotland},
  month =	 FTFJP2005date,
  abstract =	 "In this paper, I examine some of reasons that
                  ``readonly'' style qualifiers have been proposed for
                  Java, and also the principles behind the rules for
                  these new qualifiers. I find that there is a
                  mismatch between some of the motivating problems and
                  the proposed solutions. Thus I urge Java designers
                  to proceed with caution when adopting a solution to
                  these sets of problems.",
}

@article{1152650,
 author = {Atsushi Igarashi and Mirko Viroli},
 title = {Variant parametric types: A flexible subtyping scheme for generics},
 journal = TOPLAS,
 volume = {28},
 number = {5},
 year = {2006},
 issn = {0164-0925},
 pages = {795--847},
 doi = {http://doi.acm.org/10.1145/1152649.1152650},
 }

@Book{pierce:2002:types-and-pls,
  author =	 {Benjamin C. Pierce},
  title =	 {Types and Programming Languages},
  publisher =	 {MIT Press},
  year =	 2002,
  address =	 {Cambridge, MA, USA}
}

@book{Fowler2000,
  title =	 {Refactoring: Improving the Design of Existing Code},
  author =	 {Martin Fowler},
  publisher =	 {Addison-Wesley},
  year =	 {2000},
  address =	 {New York, NY, USA}
}

@InProceedings{Xie2006,
  author =	 "Tao Xie",
  title =	 "Augmenting automatically generated unit-test suites
                  with regression oracle checking",
  booktitle =	 ECOOP2006,
  pages =	 "380--403",
  year =	 2006,
  publisher =	 sv,
  address =	 sv-address,
  month =	 ECOOP2006date,
}

@Article{DoladoHOH2003,
  author = 	 "Jos{\'e} Javier Dolado and Mark Harman and Mari Carmen Otero and Lin Hu",
  title = 	 "An Empirical Investigation of the Influence of a Type of Side Effects on Program Comprehension",
  journal = 	 TSE,
  year = 	 2003,
  volume = 	 29,
  number = 	 7,
  pages = 	 "665--670",
  month = 	 jul,
  abstract =
   "This paper reports the results of a study on the impact of a type of side
    effect (SE) upon program comprehension. We applied a crossover design on
    different tests involving fragments of C code that include increment and
    decrement operators. Each test had an SE version and a side-effect-free
    counterpart. The variables measured in the treatments were the number of
    correct answers and the time spent in answering. The results show that the
    side-effect operators considered significantly reduce performance in
    comprehension-related tasks, providing empirical justification for the
    belief that side effects are harmful.",
}

@PhdThesis{Salcianu2006,
  author = 	 "Alexandru S{\u{a}}lcianu",
  title = 	 "Pointer analysis for {Java} programs: Novel techniques and applications",
  school = 	 MITEECS,
  year = 	 2006,
  address = 	 MITaddr,
  month = 	 sep,
}

@InProceedings{MarianiP2005,
  author =	 "Leonardo Mariani and Mauro Pezz{\`e}",
  title =	 "Behavior capture and test: Automated analysis of
                  component integration",
  booktitle =	 ICECCS2005,
  pages =	 "292--301",
  year =	 2005,
  publisher =	 {IEEE},
  address =	 {Tokyo, Japan},
  month =	 ICECCS2005date,
  usesDaikon =	 1,
  basefilename = "mariani-eccs-2005",
  downloads =
                  "http://www.lta.disco.unimib.it/homepage/leonardo.mariani/pdf/iceccs05.pdf
                  PDF",
  abstract =	 "Component-based technology is increasingly adopted
                  to speed up the development of complex software
                  through component reuse.  Unfortunately, the lack of
                  complete information about reused components, and
                  the complex interaction patterns among components
                  can lead to subtle problems that throw new
                  verification challenges.  Good components are often
                  re-used many times, sometimes within product lines,
                  in other cases across different products. The reuse
                  of components provides a lot of information that
                  could be useful for verification.  In this paper, we
                  show how to automatically analyze component
                  interactions by collecting information about
                  components' behavior during testing and field
                  execution, and then using the collected information
                  for checking the compatibility of components when
                  updated or reused in new products.  The paper
                  illustrates the main problems in developing the
                  idea, proposes original solutions, and presents a
                  preliminary experience that illustrates the
                  effectiveness of the approach.",
}

@Book{GoslingJSB2005,
  author =       "James Gosling and Bill Joy and Guy Steele and Gilad Bracha",
  title =        "The Java Language Specification",
  publisher =    "Addison Wesley",
  year =         2005,
  address =	 "Boston, MA",
  edition = 	 "Third",
  keywords =     "Java, Sun, book, text, computer, programming language
                 definition, PLD, object oriented, OOP, OO, zz1097",
}

@Article{BurdyEtAl05:STTT,
  author = 	 "Lilian Burdy and Yoonsik Cheon and David Cok and 
		   Michael D. Ernst and Joe Kiniry and Gary T. Leavens and 
		   K. Rustan M. Leino and Erik Poll",
  title = 	 "An overview of {JML} tools and applications",
  journal = 	 STTT,
  year = 	 2005,
  volume =	 7,
  number =	 3,
  pages =	 "212--232",
  month =	 jun,
  basefilename = "jml-tools-sttt2005",
  downloadsnonlocal =
    "http://pag.csail.mit.edu/~mernst/pubs/jml-tools-sttt2005.pdf PDF;
     http://pag.csail.mit.edu/~mernst/pubs/jml-tools-sttt2005.ps PostScript",
  category = "Verification",
  summary =
   "This paper overviews the Java Modeling Language (JML) notation for
    detailed design and gives a brief description of some of the tools that
    take it as an input or produce it as an output.",
  abstract =
   "The Java Modeling Language (JML) can be used to specify the detailed design
    of Java classes and interfaces by adding annotations to Java source
    files. The aim of JML is to provide a specification language that is easy
    to use for Java programmers and that is supported by a wide range of tools
    for specification type-checking, runtime debugging, static analysis, and
    verification.
    \par
    This paper gives an overview of the main ideas behind JML, details
    about JML's wide range of tools, and a glimpse into existing
    applications of JML.",
  usesDaikon = 1,
}

@InProceedings{ArtziEGKPP2006,
  author = 	 "Shay Artzi and Michael D. Ernst and Adam Kie{\.z}un and Carlos Pacheco and Jeff H. Perkins",
  authorASCII =  "Adam Kiezun",
  title = 	 "Finding the needles in the haystack: Generating legal test inputs for object-oriented programs",
  booktitle = MTOOS2006,
  NEEDpages = 	 "*",
  year = 	 2006,
  address = 	 {Portland, Oregon, USA},
  month = 	 MTOOS2006date,
  publisher = acm,
  abstract =
   "A test input for an object-oriented program typically consists of a
    sequence of method calls that use the API defined by the program
    under test. Generating legal test inputs can be challenging because,
    for some programs, the set of legal method sequences is much smaller
    than the set of all possible sequences; without a formal
    specification of legal sequences, an input generator is bound to
    produce mostly illegal sequences.
    \par
    We propose a scalable technique that combines dynamic analysis with
    random testing to help an input generator create legal test inputs
    without a formal specification, even for programs in which
    most sequences are illegal. The technique uses an example execution
    of the program to infer a model of legal call sequences, and uses
    the model to guide a random input generator towards legal but
    behaviorally-diverse sequences.
    \par
    We have implemented our technique for Java, in a tool called
    Palulu, and evaluated its effectiveness in creating legal inputs
    for real programs. Our experimental results indicate that the
    technique is effective and scalable. Our preliminary evaluation
    indicates that the technique can quickly generate legal sequences
    for complex inputs: in a case study, Palulu created legal test
    inputs in seconds for a set of complex classes, for which it took an
    expert thirty minutes to generate a single legal input.",
  basefilename = "oo-test-gen-mtoos2006",
  downloadsnonlocal =
    "http://pag.csail.mit.edu/~mernst/pubs/oo-test-gen-mtoos2006.pdf PDF;
     http://pag.csail.mit.edu/~mernst/pubs/oo-test-gen-mtoos2006.ps PostScript",
  category =     "Testing",
  summary =
   "An automatically inferred model of legal method call sequences can bias test
    generation toward legal method sequences, increasing coverage and creating
    data structures beyond the ability of undirected random generation.",
}

@Article{ErnstCGN2001:TSE,
  author = 	 "Michael D. Ernst and Jake Cockrell and
		  William G. Griswold and David Notkin", 
  title = 	 "Dynamically discovering likely program invariants to
		  support program evolution",
  journal = 	 TSE,
  year = 	 2001,
  volume =	 27,
  number =	 2,
  pages =	 "99--123",
  month = 	 feb,
  note = 	 ErnstCGN2001TSEnote,
  abstract = 
   "Explicitly stated program invariants can help programmers by identifying
    program properties that must be preserved when modifying code.  In
    practice, however, these invariants are usually implicit.  An alternative
    to expecting programmers to fully annotate code with invariants is to
    automatically infer likely invariants from the program itself.  This
    research focuses on dynamic techniques for discovering invariants from
    execution traces.
    \par
    This article reports three results.  First, it describes techniques for
    dynamically discovering invariants, along with an implementation, named
    Daikon, that embodies these techniques.  Second, it reports on the
    application of Daikon to two sets of target programs.  In programs from
    Gries's work on program derivation, the system rediscovered predefined
    invariants.  In a C program lacking explicit invariants, the system
    discovered invariants that assisted a software evolution task.  These
    experiments demonstrate that, at least for small programs, invariant
    inference is both accurate and useful.  Third, it analyzes scalability
    issues such as invariant detection runtime and accuracy as functions of
    test suites and program points instrumented.",
  basefilename = "invariants-tse2001",
  downloadsnonlocal =
    "http://pag.csail.mit.edu/~mernst/pubs/invariants-tse2001.pdf PDF",
  downloads =
    "http://pag.csail.mit.edu/~mernst/pubs/invariants-icse99-slides.ppt ICSE 1999 talk slides (PowerPoint);
     http://pag.csail.mit.edu/~mernst/pubs/invariants-icse99-slides.ps ICSE 1999 talk slides (PostScript);
     http://pag.csail.mit.edu/daikon/ Implementation",
  category = "Invariant detection",
  summary =
   "Program properties (such as formal specifications or assert statements)
    are useful for a variety of programming tasks.  This paper shows how to
    dynamically infer program properties by looking for patterns and
    relationships among values computed at run time.",
}

@Misc{JSR308-2008-09-12,
  author = 	 "Michael D. Ernst",
  title = 	 "Type Annotations specification (JSR 308)",
  howpublished = "\url{http://pag.csail.mit.edu/jsr308/}",
  month = 	 sep # "~12,",
  year = 	 2008,
  NOabstract =   1,
  basefilename = "annotations-jsr308",
  category =     "Programming language design",
  summary =
   "This specification extends Java's annotation system to permit annotations
    on any use of a type (including generic type arguments, method receivers,
    etc.).  It is planned for inclusion in Java 7, but it is usable immediately
    with full backward compatibility with existing compilers and JVMs.",
  downloads =
    "http://pag.csail.mit.edu/jsr308/ current status and implementation;
     http://jcp.org/en/jsr/detail?id=308 original proposal",
}

@InProceedings{TschantzE2005,
  author =	 "Matthew S. Tschantz and Michael D. Ernst",
  title =	 "Javari: Adding reference immutability to {Java}",
  booktitle =	 OOPSLA2005,
  pages =	 "211--230",
  year =	 2005,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA2005date,
  basefilename = "ref-immutability-oopsla2005",
  alsosee =	 "Tschantz2006",
  downloads =
                  "http://pag.csail.mit.edu/pubs/tschantz-refimmut-mengthesis.pdf
                  extended version (PDF)",
  downloadsnonlocal
                  ="http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2005.pdf
                  PDF;
                  http://pag.csail.mit.edu/pubs/tschantz-refimmut-mengthesis.pdf
                  extended version (PDF);
                  http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2005-slides.ppt
                  slides (PowerPoint)",
  category =	 "Programming language design",
  summary =	 "A compiler can guarantee that an immutable reference
                  is not used to cause side effects to any reachable
                  object. This paper extends previous proposals in
                  many ways, including formal type rules and support
                  for Java generics.",
  abstract =	 "This paper describes a type system that is capable
                  of expressing and enforcing immutability
                  constraints.  The specific constraint expressed is
                  that the abstract state of the object to which an
                  immutable reference refers cannot be modified using
                  that reference.  The abstract state is (part of) the
                  transitively reachable state: that is, the state of
                  the object and all state reachable from it by
                  following references.  The type system permits
                  explicitly excluding fields from the abstract state
                  of an object.  For a statically type-safe language,
                  the type system guarantees reference immutability.
                  If the language is extended with immutability
                  downcasts, then run-time checks enforce the
                  reference immutability constraints.  \par This
                  research builds upon previous research in language
                  support for reference immutability.  Improvements
                  that are new in this paper include distinguishing
                  the notions of assignability and mutability;
                  integration with Java 5's generic types and with
                  multi-dimensional arrays; a mutability polymorphism
                  approach to avoiding code duplication; type-safe
                  support for reflection and serialization; and formal
                  type rules and type soundness proof for a core
                  calculus.  Furthermore, it retains the valuable
                  features of the previous dialect, including
                  usability by humans (as evidenced by experience with
                  160,000 lines of Javari code) and interoperability
                  with Java and existing JVMs.",
}

@PhdThesis{Boyapati2004:PhD,
  author = 	 "Chandrasekhar Boyapati",
  title = 	 "{SafeJava}: A Unified Type System for Safe Programming",
  school = 	 MITEECS,
  year = 	 2004,
  address = 	 MITaddr,
  month = 	 feb,
}

@InProceedings{lu:2006:owner-accessiblity,
  author =	 "Yi Lu and John Potter",
  title =	 "On ownership and accessibility",
  booktitle =	 ECOOP2006,
  pages =	 "99--123",
  year =	 2006,
  publisher =	 sv,
  address =	 sv-address,
  month =	 ECOOP2006date,
}

@InProceedings{BoyapatiLS2003,
  author = 	 "Chandrasekhar Boyapati and Barbara Liskov and Liuba Shrira",
  title = 	 "Ownership types for object encapsulation",
  booktitle =	 POPL2003,
  pages =	 "213--223",
  year =	 2003,
  address =	 POPL2003addr,
  month =	 POPL2003date
}

@InProceedings{TkachukD03,
  author =	 "Oksana Tkachuk and Matthew B. Dwyer",
  title =	 "Adapting side effects analysis for modular program
                  model checking",
  booktitle =	 FSE2003,
  pages =	 "188--197",
  year =	 2003,
  publisher =	 acm,
  address =	 acm-address,
  month =	 FSE2003date,
}

@article{Clausen97,
  author    = "Lars R. Clausen",
  title     = "A {Java} bytecode optimizer using side-effect analysis",
  journal   = CPE,
  volume    = 9,
  number    = 11,
  year      = 1997,
  pages     = {1031-1045},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  abstract =
   "This paper describes Cream, an optimizer for Java bytecode using
    side-effect analysis to improve the optimizations. Dead-code elimination
    and loop-invariant removal are implemented and tested, as well as several
    variations of the side-effect analysis. The optimizer is tested on
    real-world applications such as itself and JavaSoft’s Java
    compiler. Results show that the optimizations benefit well from the
    side-effect analysis. The best side-effect analysis gives five to ten times
    as many optimizations as without an analysis, and, in one case, makes a
    speed increase of 25\% possible.",
}

@InProceedings{DallmeierLWZ2006,
  author =	 "Valentin Dallmeier and Christian Lindig and Andrzej
                  Wasylkowski and Andreas Zeller",
  title =	 "Mining object behavior with {ADABU}",
  booktitle =	 WODA2006,
  pages =	 "17--24",
  year =	 2006,
  publisher =	 acm,
  address =	 acm-address,
  month =	 WODA2006date,
}

@InProceedings{BirkaE2004,
  author =	 "Adrian Birka and Michael D. Ernst",
  title =	 "A practical type system and language for reference
                  immutability",
  booktitle =	 OOPSLA2004,
  pages =	 "35--49",
  year =	 2004,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA2004date,
  basefilename = "ref-immutability-oopsla2004",
  downloadsnonlocal
                  ="http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2004.pdf
                  PDF;
                  http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2004.ps
                  PostScript;
                  http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2004-slides.pdf
                  slides (PDF);
                  http://pag.csail.mit.edu/~mernst/pubs/ref-immutability-oopsla2004-slides.ps
                  slides (PostScript)",
  category =	 "Programming language design",
  summary =	 "This paper presents a type system, language,
                  implementation, and evaluation of a safe mechanism
                  for enforcing reference immutability, where an
                  immutable reference may not be used to cause side
                  effects to any object reachable from it.",
  abstract =	 "This paper describes a type system that is capable
                  of expressing and enforcing immutability
                  constraints.  The specific constraint expressed is
                  that the abstract state of the object to which an
                  immutable reference refers cannot be modified using
                  that reference.  The abstract state is (part of) the
                  transitively reachable state: that is, the state of
                  the object and all state reachable from it by
                  following references.  The type system permits
                  explicitly excluding fields or objects from the
                  abstract state of an object.  For a statically
                  type-safe language, the type system guarantees
                  reference immutability.  If the language is extended
                  with immutability downcasts, then run-time checks
                  enforce the reference immutability constraints.
                  \par In order to better understand the usability and
                  efficacy of the type system, we have implemented an
                  extension to Java, called Javari, that includes all
                  the features of our type system.  Javari is
                  interoperable with Java and existing JVMs.  It can
                  be viewed as a proposal for the semantics of the
                  Java \texttt{const} keyword, though Javari's syntax
                  uses \texttt{readonly} instead.  This paper
                  describes the design and implementation of Javari,
                  including the type-checking rules for the language.
                  This paper also discusses experience with 160,000
                  lines of Javari code.  Javari was easy to use and
                  provided a number of benefits, including detecting
                  errors in well-tested code.",
  usesDaikonAsTestSubject =1,
}

@InProceedings{BoylandNR2001,
  author =	 "John Boyland and James Noble and William Retert",
  title =	 "Capabilities for sharing: A generalisation of
                  uniqueness and read-only",
  booktitle =	 ECOOP2001,
  pages =	 "2--27",
  year =	 2001,
  publisher =	 sv,
  address =	 sv-address,
  month =	 ECOOP2001date,
  abstract =	 "Many languages and language extensions include
                  annotations on pointer variables such as
                  ``read-only,'' ``unique,'' and ``borrowed''; many
                  more annotations have been proposed but not
                  implemented. Unfortunately, all these annotations
                  are described individually and formalised
                  independently - assuming they are formalised at
                  all. In this paper, we show how these annotations
                  can be subsumed into a general capability system for
                  pointers. This system separates mechanism (defining
                  the semantics of sharing and exclusion) from policy
                  (defining the invariants that are intended to be
                  preserved). The capability system has a well-defined
                  semantics which can be used as a reference for the
                  correctness of various extended type systems using
                  annotations. Furthermore, it supports research in
                  new less-restrictive type systems that permit a
                  wider range of idioms to be statically checked."
}

@Misc{JSR133,
  author =       "William Pugh",
  title =        "{JSR} 133: \textsc{Java} Memory Model and Thread Specification Revision",
  howpublished = "\url{http://jcp.org/en/jsr/detail?id=133}",
  month =        sep # "~30,",
  year =         2004,
}

@InProceedings{FahndrichL2003,
  author =	 "Manuel F{\"a}hndrich and K. Rustan M. Leino",
  authorASCII =	 "Manuel Fahndrich",
  title =	 "Declaring and checking non-null types in an
                  object-oriented language",
  booktitle =	 OOPSLA2003,
  pages =	 "302--312",
  year =	 2003,
  publisher =	 acm,
  address =	 acm-address,
  month =	 OOPSLA2003date,
  abstract =	 "Distinguishing non-null references from
                  possibly-null references at the type level can
                  detect null-related errors in object-oriented
                  programs at compile-time. This paper gives a
                  proposal for retrofitting a language such as C# or
                  Java with non-null types. It addresses the central
                  complications that arise in constructors, where
                  declared non-null fields may not yet have been
                  initialized, but the partially constructed object is
                  already accessible. The paper reports experience
                  with an implementation for annotating and checking
                  null-related properties in C# programs.",
}

@InProceedings{HuangZS2007:cJ,
  author =	 "Shan Shan Huang and David Zook and Yannis
                  Smaragdakis",
  title =	 "{cJ}: Enhancing {Java} with safe type conditions",
  booktitle =	 AOSD2007,
  pages =	 "185--198",
  year =	 2007,
  publisher =	 acm,
  address =	 acm-address,
  month =	 AOSD2007date,
  abstract =	 "cJ is an extension of Java that allows supertypes,
                  fields, and methods of a class or interface to be
                  provided only under some static subtyping
                  condition. For instance, a cJ generic class, C<P>,
                  may provide a member method m only when the type
                  provided for parameter P is a subtype of a specific
                  type Q.  \par From a practical standpoint, cJ adds
                  to generic Java classes and interfaces the ability
                  to express case-specific code. Unlike conditional
                  compilation techniques (e.g., the C/C++ ``#ifdef''
                  construct) cJ is statically type safe and maintains
                  the modular type-checking properties of Java generic
                  classes: a cJ generic class can be checked
                  independently of the code that uses it. Just like
                  regular Java, checking a cJ class implies that all
                  uses are safe, under the contract for type
                  parameters specified in the class's signature.  \par
                  As a specific application, cJ addresses the
                  well-known shortcomings of the Java Collections
                  Framework (JCF). JCF data structures often throw
                  run-time errors when an ``optional'' method is
                  called upon an object that does not support
                  it. Within the constraints of standard Java, the
                  authors of the JCF had to either sacrifice static
                  type safety or suffer a combinatorial explosion of
                  the number of types involved. cJ avoids both
                  problems, maintaining both static safety and
                  conciseness.",
}

@InProceedings{deline04typestates,
  author =	 "Robert DeLine and Manuel F{\"a}hndrich",
  title =	 "Typestates for objects",
  booktitle =	 ECOOP2004,
  pages =	 "465--490",
  year =	 2004,
  publisher =	 sv,
  address =	 sv-address,
  month =	 ECOOP2004date,
}

@Book{Bloch2001,
  author = 	 "Joshua Bloch",
  title = 	 "Effective {Java} Programming Language Guide",
  publisher = 	 "Addison Wesley",
  year = 	 "2001",
  address = 	 "Boston, MA",
}
@TechReport{Birka2003:TR,
  author = 	 "Adrian Birka",
  title = 	 "Compiler-enforced immutability for the {Java} language",
  institution =  MITLCS,
  year = 	 2003,
  number =	 "MIT-LCS-TR-908",
  address =	 MITaddr,
  month =	 jun,
  note =         "Revision of Master's thesis",
  supersededby = "BirkaE2004",
  abstract =
   "This thesis presents the design, implementation, and evaluation of an
    extension to the Java language, ConstJava, that is capable of expressing
    immutability constraints and verifying them at compile time.  The
    specific constraint expressed in ConstJava is that the transitive state of
    the object to which a given reference refers cannot be modified using
    that reference.
    \par
    In addition to the ability to specify and enforce this basic
    constraint, ConstJava includes several other features, such as mutable
    fields, immutable classes, templates, and the const\_cast operator,
    that make ConstJava a more useful language.  
    \par
    The thesis evaluates the utility of ConstJava via experiments involving
    writing ConstJava code and converting Java code to ConstJava code.  The
    evaluation of ConstJava shows that the language provides tangible
    benefits in early detection and correction of bugs that would
    otherwise be difficult to catch.  There are also costs associated with
    the use of ConstJava.  These are minimized by ConstJava's backward
    compatibility with Java, and by the high degree of inter-operability
    of the two languages, which allows for a less painful transition from
    Java to ConstJava.
    \par
    This technical report is a revision of the author's Master's thesis,
    which was advised by Prof.~Michael D.~Ernst.",
  basefilename = "immutability-tr908",
  category = "Programming language design",
  summary =
   "This thesis presents a language (ConstJava), type system, implementation,
    and evaluation of a safe mechanism for enforcing reference immutability,
    where an immutable pointer may not be used to cause side effects to any
    object reachable from it.",
}
@Book{GoslingJSB2000,
  author =       "James Gosling and Bill Joy and Guy Steele and Gilad Bracha",
  title =        "The Java Language Specification",
  publisher =    "Addison Wesley",
  year =         2000,
  address =	 "Boston, MA",
  edition = 	 "Second",
  keywords =     "Java, Sun, book, text, computer, programming language
                 definition, PLD, object oriented, OOP, OO, zz1097",
  ISBN     =     "0-201-63451-1",
}
@TechReport{MuellerPoetzsch-Heffter01a,
  author      = { M{\"u}ller, P. and Poetzsch-Heffter, A. },
  title       = { Universes: A Type System
                 for Alias and Dependency Control },
  institution = { Fernuniversit{\"a}t Hagen },
  year        = 2001,
  number      = 279,
  note        = {  }
}
@InProceedings{PoratBKM2000,
  author = 	 "Sara Porat and Marina Biberstein and Larry Koved and
                  Bilba Mendelson",
  title = 	 "Automatic detection of immutable fields in {Java}",
  NEEDpages = 	 "",
  booktitle =	 CASCON2000,
  year =	 2000,
  address =	 CASCON2000addr,
  month =	 CASCON2000date,
  abstract =
   "This paper introduces techniques to detect mutability of fields and classes
    in Java. A variable is considered to be mutable if a new value is stored
    into it, as well as if any of its reachable variables is mutable. We
    present a static flow-sensitive analysis algorithm which can be applied to
    any Java component. The analysis classifies fields and classes as either
    mutable or immutable. In order to facilitate open-world analysis, the
    algorithm identifies situations that expose variables to potential
    modification by code outside the component, as well as situations where
    variables are modified by the analyzed code. We also present an
    implementation of the analysis which focuses on detecting mutability of
    class variables, so as to avoid isolation problems. The implementation
    incorporates intra- and inter-procedural data-flow analyses and is shown to
    be highly scalable. Experimental results demonstrate the effectiveness of
    the algorithms."
}
@InProceedings{FosterFFA99,
  author =    "Jeffrey S. Foster and Manuel F{\"{a}}hndrich and
               Alexander Aiken",
  title =     "A theory of type qualifiers",
  pages =     "192--203",
  booktitle = PLDI99,
  year =      1999,
  address =   PLDI99addr,
  month =     PLDI99date
}

@InProceedings{LucassenG88,
  author = 	 "John M. Lucassen and David K. Gifford",
  title = 	 "Polymorphic effect systems",
  booktitle =	 POPL88,
  pages =	 "47--57",
  year =	 1988,
  address =	 POPL88addr,
  month =	 POPL88date
}
@InProceedings{TalpinJ92,
  author = 	 "Jean-Pierre Talpin and Pierre Jouvelot",
  title = 	 "The type and effect discipline",
  booktitle =	 LICS92,
  pages =	 "162--173",
  year =	 1992,
  address =	 LICS92addr,
  month =	 LICS92date
}
@InCollection{NiNi99tes,
  author =       "F. Nielson and H. R. Nielson",
  title =        "Type and Effect Systems",
  booktitle =    "Correct System Design",
  publisher =    "Springer-Verlag",
  year =         1999,
  OMITeditor =       "E. R. Olderog and B. Steffen",
  number =       1710,
  series =       LNCS,
  pages =        "114--136",
  abstract =
   "The design and implementation of a correct system can benefit 
    from employing static techniques for ensuring that the dynamic 
    behaviour satisfies the specification. Many programming languages 
    incorporate types for ensuring that certain operations are only
    applied to data of the appropriate form. A natural extension of 
    type checking techniques is to enrich the types with annotations 
    and effects that further describe intensional aspects of the dynamic 
    behaviour.",
}
@Book{MilnerTH90,
  author =   "Robin Milner and Mads Tofte and Robert Harper",
  title =    "The Definition of Standard {ML}",
  publisher =    "MIT Press",
  year =     1990
}
@Manual{OCaml:Manual,
  title =    "The Objective Caml system, release 3.07",
  OPTkey =   "",
  author =   "Xavier Leroy",
  OPTorganization = "",
  OPTaddress =   "",
  OPTedition =   "",
  month =    sep # "~29,",
  year =     2003,
  note =     "with Damien Doligez, Jacques Garrigue, Didier R{\'e}my and J{\'e}r{\^o}me Vouillon",
  OPTannote =    ""
}
@Book{Stroustrup00:CPL,
  author =	 "Bjarne Stroustrup",
  title = 	 "The C++ Programming Language",
  publisher = 	 "Addison-Wesley",
  year = 	 2000,
  address =	 "Boston, MA",
  edition =	 "Special"
}
@Book{KernighanR88,
  author = 	 "Brian W. Kernighan and Dennis M. Ritchie",
  title = 	 "The {C} Programming Language",
  publisher = 	 "Prentice Hall",
  year = 	 1988,
  series =	 "Software Series",
  address =	 "Englewood Cliffs, New Jersey",
  edition =	 "Second"
}
@Book{Meyers97,
  author =	 "Scott Meyers",
  title = 	 "Effective C++",
  publisher = 	 "Addison-Wesley",
  year = 	 1997,
  NEEDaddress = 	 "",
  edition =	 "second"
}
@Misc{Morris1978,
  author =	 "James H. Morris",
  title =	 "Sniggering Type Checker experiment",
  howpublished = "Experiment at Xerox PARC",
  year =	 1978,
  note =	 "Personal communication, May 2004"
}
@Article{Gannon77,
  author = 	 "John D. Gannon",
  title = 	 "An experimental evaluation of data type conventions",
  journal = 	 CACM,
  year = 	 1977,
  volume =	 20,
  number =	 8,
  pages =	 "584--595",
  month =	 aug
}
@Article{PrecheltT98,
  author = 	 "Lutz Prechelt and Walter F. Tichy",
  title = 	 "A Controlled Experiment to Assess the Benefits of
                  Procedure Argument Type Checking",
  journal = 	 TSE,
  year = 	 1998,
  volume =	 24,
  number =	 4,
  pages =	 "302--312",
  month =	 apr,
  abstract =
   "Type checking is considered an important mechanism for detecting
    programming errors, especially interface errors. This report describes an
    experiment to assess the defect-detection capabilities of static,
    intermodule type checking. The experiment uses ANSI C and Kernighan&Ritchie
    (K&R) C. The relevant difference is that the ANSI C compiler checks module
    interfaces (i.e., the parameter lists calls to external functions), whereas
    K&R C does not. The experiment employs a counterbalanced design in which
    each of the 40 subjects, most of them CS PhD students, writes two
    nontrivial programs that interface with a complex library (Motif). Each
    subject writes one program in ANSI C and one in K&R C. The input to each
    compiler run is saved and manually analyzed for defects. Results indicate
    that delivered ANSI C programs contain significantly fewer interface
    defects than delivered K&R C programs. Furthermore, after subjects have
    gained some familiarity with the interface they are using, ANSI C
    programmers remove defects faster and are more productive (measured in both
    delivery time and functionality implemented).",
}
@InProceedings{ClarkeNP2001,
  author = 	 "David G. Clarke and James Noble and John M. Potter",
  title = 	 "Simple ownership types for object containment",
  booktitle =	 ECOOP2001,
  pages =	 "53--76",
  year =	 2001,
  address =	 ECOOP2001addr,
  month =	 ECOOP2001date
}
@InProceedings{AldrichKC2002,
  author = 	 "Jonathan Aldrich and Valentin Kostadinov and Craig Chambers",
  title = 	 "Alias annotations for program understanding",
  booktitle =	 OOPSLA2002,
  pages =	 "311--330",
  year =	 2002,
  address =	 OOPSLA2002addr,
  month =	 OOPSLA2002date
}
@InProceedings{Boyland2003,
  author = 	 "John Boyland",
  title = 	 "Checking interference with fractional permissions",
  booktitle =	 SAS2003,
  pages =	 "55--72",
  year =	 2003,
  address =	 SAS2003addr,
  month =	 SAS2003date
}
@InProceedings{Wadler90,
  author = 	 "Philip Wadler",
  title = 	 "Linear types can change the world!",
  booktitle =	 "{IFIP {TC} 2} Working Conference on Programming Concepts and Methods",
  pages =	 "347--359",
  year =	 1990,
  OMITeditor = 	 "M. Broy and C. Jones",
  address =	 "Sea of Galilee, Israel",
  month =	 apr,
  abstract =
   "The linear logic of J.-Y. Girard suggests a new type system for functional
    languages, one which supports operations that ``change the world''. Values
    belonging to a linear type must be used exactly once: like the world, they
    cannot be duplicated or destroyed. Such values require no reference
    counting or garbage collection, and safely admit destructive array
    update. Linear types extend Schmidt's notion of single threading; provide
    an alternative to Hudak and Bloss' update analysis; and offer a practical
    complement to Lafont and Holmström's elegant linear languages."
}


@InProceedings{FahndrichD2002,
  author = 	 "Manuel F{\"a}hndrich and Robert DeLine",
  title = 	 "Adoption and focus: Practical linear types for imperative programming",
  booktitle =	 PLDI2002,
  pages =	 "13--24",
  year =	 2002,
  address =	 PLDI2002addr,
  month =	 PLDI2002date
}
